분리 논리
- 논리 체계
분리 논리(separation logic)는 부분 구조 논리에 기반한 호어 로직의 변형이다.
동기
다음과 같은 호어 트리플을 생각해보자. \[ \newcommand{\triple}[3] {\{#1\} \ #2 \ \{#3\}} \newcommand{\read}[1] {\textbf{read}(#1)} \newcommand{\store}[2] {\textbf{store}(#1, #2)} \triple {\ell_1 \mapsto v_1 \wedge \ell_2 \mapsto v_2} { x \leftarrow \read{\ell_1} + 1; \ \store{\ell_2}{x} } {\ell_1 \mapsto v_1 \wedge \ell_2 \mapsto v_1 + 1} \] 이는 언뜻 올바른 스펙 같아 보이지만, \(\ell_1 = \ell_2\) 인 경우 성립하지 않는다. 이렇게 서로 다른 포인터 변수가 같은 주소값을 가지는 상황을 포인터 에일리어싱(pointer aliasing) 이라고 한다.
분리 논리에서는 분리 연언을 이용해 포인터 에일리어싱이 발생하지 않음을 가정할 수 있다. \[ \triple {\ell_1 \mapsto v_1 * \ell_2 \mapsto v_2} { x \leftarrow \read{\ell_1} + 1; \ \store{\ell_2}{x} } {\ell_1 \mapsto v_1 * \ell_2 \mapsto v_1 + 1} \]
연결사
분리 연언 (separating conjunction)
\[ \phi * \psi \]
분리 함언 (separating implication, magic wand)
\[ \newcommand{\wand}[0] {\mathbin{- \!\! *}} \phi \wand \psi \]
Points-to
\[ \ell \mapsto v \]
분수 권한(fractional permission) points-to
\[ \newcommand{\pt}[1] {\overset{#1}{\mapsto}} \ell \pt{q} v \]